Termination Proof Script

Consider the TRS R consisting of the rewrite rules

There are 10 dependency pairs:

The approximated dependency graph contains one SCC: {4,7,10-13}.

Consider the SCC {4,7,10-13}. By taking the AF π with π(a) = π(A) = π(b) = 1 together with the lexicographic path order with precedence f ≈ F, the rules in {1-4,11-13} are weakly decreasing and the rules in {7,10} are strictly decreasing. There is one new SCC.
- Consider the SCC {4,11-13}. The constraints could not be solved.

Tyrolean Termination Tool (0.70 seconds) --- May 4, 2006